Nuprl Lemma : strict-fun-connected_transitivity3
11,40
postcript
pdf
T
:Type,
f
:(
T
T
). retraction(
T
;
f
)
(
x
,
y
,
z
:
T
.
y
=
f
+(
x
)
z
is
f
*(
y
)
z
=
f
+(
x
))
latex
Definitions
s
=
t
,
t
T
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
y
is
f
*(
x
)
,
,
A
,
x
:
A
B
(
x
)
,
P
&
Q
,
Type
,
retraction(
T
;
f
)
,
Void
,
P
Q
,
False
,
y
=
f
+(
x
)
Lemmas
fun-connected
transitivity
,
fun-connected
antisymmetry
,
false
wf
,
retraction
wf
,
not
wf
,
fun-connected
wf
origin
T:Type, f:(T
T). retraction(T;f) 
(x, y, z:T. y = f+(x) z is f*(y) z = f+(x)) T:Type, f:(TT). retraction(T;f) (x, y, z:T. y = f+(x) z is f*(y) z = f+(x)) 
TB(x)x:A. B(x)
A
B(x) Q